#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include "klee_change_macros.h"
#include "klee_change_functions.h"
int lib(int x) {
	if (x < 0){
		return -x;
	}
	if(klee_change(0,1)){
		int counter = 0;
	    while (x > 0) {
	        x += 1;
	    	counter += 1;
    	}
	    return counter;
	}
	else{
		return x;
	}
}

int client(int x){
	if (x < 0) {
		return lib(x);
	}
	return -x;
}

int main(int argc, char *argv[]) {
  int x= atoi(argv[1]);
  return client(x);
}
